Inference at * 1 1 1 2 
Iof proof for Lemma comp nat ind tp:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. i : 
4. zz,i:. (i < zz)  P(i)
  P(i) 

latex

 by (\p.let i = mvt (var_of_hyp (-2) p) in 
 blet ip1 = mk_add_term  i 1 in 
 b((DTerm ip1 (-1))

CollapseTHENM (DTerm i (-1))) p) 

latex

C1: .....wf..... NILNIL

C1: 3. i : 
C1:   (i + 1)  
C2: .....wf..... NILNIL

C2: 3. i : 
C2:   i  
C3: 

C3: 4. (i < (i + 1))  P(i)
C3:   P(i)
C.

Definitions

x:A. B(x), t  T